@INPROCEEDINGS{ripple-analysis,
    author = {Alan Bundy and Frank Van Harmelen and Jane Hesketh and Alan Smaill and Andrew Stevens},
    title = {A Rational Reconstruction and Extension of Recursion Analysis},
    booktitle = {Proceedings of the Eleventh International Joint Conference on Artificial Intelligence},
    year = {1992},
    pages = {359--365},
    publisher = {Morgan Kaufmann}
}

@inproceedings{quickcheck,
 author = {Claessen, Koen and Hughes, John},
 title = {QuickCheck: a lightweight tool for random testing of Haskell programs},
 booktitle = {Proceedings of the fifth ACM SIGPLAN international conference on Functional programming},
 series = {ICFP '00},
 year = {2000},
 pages = {268--279},
 numpages = {12},
 publisher = {ACM},
 address = {New York, NY, USA},
} 

@inproceedings{smallcheck,
 author = {Runciman, Colin and Naylor, Matthew and Lindblad, Fredrik},
 title = {Smallcheck and lazy smallcheck: automatic exhaustive testing for small values},
 booktitle = {Proceedings of the first ACM SIGPLAN symposium on Haskell},
 series = {Haskell '08},
 year = {2008},
 pages = {37--48},
 numpages = {12},
 publisher = {ACM},
 address = {New York, NY, USA}
} 

@inproceedings{clam,
 author = {Bundy, Alan},
 title = {The Use of Explicit Plans to Guide Inductive Proofs},
 booktitle = {Proceedings of the 9th International Conference on Automated Deduction},
 year = {1988},
 isbn = {3-540-19343-X},
 pages = {111--120},
 numpages = {10},
 url = {http://portal.acm.org/citation.cfm?id=648228.752123},
 acmid = {752123},
 publisher = {Springer-Verlag},
 address = {London, UK},
} 


@manual{isabellehol,
  title =         {Isabelle HOL - A Proof Assistant for Higher-Order Logic},
  author =        {Tobias Nipkow, Lawrence C. Paulson, Markus Wenzel},
  month =         {April},
  year =          {2009},
  organization =  {University of Cambridge, Universit\"{a}t M\"{u}nchen},
  url =           "\url{http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle/doc/tutorial.pdf}}



@article{acl2s,
author = {Peter C. Dillinger and Panagiotis Manolios and Daron Vroon and J. Strother Moore},
title = {{ACL2s: ``The ACL2 Sedan''}},
journal ={International Conference on Software Engineering Companion},
year = {2007},
pages = {59-60},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA}
}

@inproceedings{versitility-heuristic,
 author = {Manning, Alistair and Ireland, Andrew and Bundy, Alan},
 title = {Incresing the Versatility of Heuristic Based Theorem Provers},
 booktitle = {Proceedings of the 4th International Conference on Logic Programming and Automated Reasoning},
 year = {1993},
 isbn = {3-540-56944-8},
 pages = {194--204},
 numpages = {11},
 url = {http://portal.acm.org/citation.cfm?id=645707.664139},
 acmid = {664139},
 publisher = {Springer-Verlag},
 address = {London, UK},
} 

@MISC{rippling,
    author = {Alan Bundy and Andrew Stevens and Frank Van Harmelen and Andrew Ireland and Alan Smaill},
    title = {{Rippling: A Heuristic for Guiding Inductive Proofs}},
    year = {1993}
}

@inproceedings{holacl2,
 author = {Gordon, Michael J. C. and Reynolds, James and Hunt, Warren A. and Kaufmann, Matt},
 title = {{An Integration of HOL and ACL2}},
 booktitle = {Proceedings of the Formal Methods in Computer Aided Design},
 series = {FMCAD '06},
 year = {2006},
 isbn = {0-7695-2707-8},
 pages = {153--160},
 numpages = {8},
 acmid = {1190853},
 publisher = {IEEE Computer Society},
 address = {Washington, DC, USA},
} 


@inproceedings{caseanalysisrippling,
  author    = {Moa Johansson and
               Lucas Dixon and
               Alan Bundy},
  title     = {{Case-Analysis for Rippling and Inductive Proof}},
  booktitle = {ITP},
  year      = {2010},
  pages     = {291-306},
  ee        = {http://dx.doi.org/10.1007/978-3-642-14052-5_21},
  crossref  = {DBLP:conf/itp/2010},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{isabelle,
    author = {Lawrence C. Paulson},
    title = {The Foundation of a Generic Theorem Prover},
    journal = {Journal of Automated Reasoning},
    year = {1989},
    volume = {5}
}

@ARTICLE{productivefailure,
    author = {Andrew Ireland and Alan Bundy},
    title = {Productive Use of Failure in Inductive Proof},
    journal = {Journal of Automated Reasoning},
    year = {1995},
    volume = {16},
    pages = {16-1}
}

@misc{haskell98,
  title = "{Haskell}~98 - {A} Non-strict, Purely Functional Language",
  year = "1999",
  editor = "{Peyton Jones}, Simon and Hughes, John",
  howpublished = "Available from \url{http://www.haskell.org/definition}",
  month = "February",
}

@INPROCEEDINGS{isaplanner,
    author = {Lucas Dixon and Jacques Fleuriot},
    title = {{IsaPlanner} - A prototype proof planner in {Isabelle}},
    booktitle = {Proceedings of CADE03, LNCS},
    year = {2003},
    pages = {279-283},
    publisher = {Springer}
}

@INPROCEEDINGS{Bundy01theautomation,
    author = {Alan Bundy},
    title = {The automation of proof by mathematical induction},
    booktitle = {Handbook of Automated Reasoning, volume I, chapter 13},
    year = {2001},
    pages = {845-911},
    publisher = {Elsevier Science}
}


@article{SpecSharp,
 author = {M. Barnett and M. F\"ahndrich and K. R. M. Leino and P. M\"uller and W. Schulte and H. Venter},
 title = {Specification and Verification: The Spec\# Experience},
 journal = {Communications of the ACM},
 month = {},
 year = {2010},
 volume = {},
 number = {},
 pages = {},
 publisher = {ACM},
 note = {To appear}
}

@misc{Cracatoa,
  author = {Claude March\'e},
  title = {The {Krakatoa} tool for Deductive Verification of {Java}
                  Programs},
  howpublished = {Winter School on Object-Oriented Verification,
                  Viinistu, Estonia},
  month = jan,
  year = 2009,
  url = {http://krakatoa.lri.fr/ws/},
  x-pdf = {http://krakatoa.lri.fr/ws/notes.pdf},
  note = {\url{http://krakatoa.lri.fr/ws/}},
  topics = {team},
  x-equipes = {demons PROVAL},
  x-support = {diffusion},
  x-type = {invitation}
}

@INPROCEEDINGS{Ganzinger04dpll(t):fast,
    author = {Harald Ganzinger and George Hagen and Robert Nieuwenhuis and Albert Oliveras and Cesare Tinelli},
    title = {{DPLL(T): Fast Decision Procedures}},
    booktitle = {},
    year = {2004},
    pages = {175-188},
    publisher = {Springer}
}

@MISC{acl2,
    author = {Robert S. Boyer and J Strother Moore},
    title = {A Theorem Prover for a Computational Logic},
    year = {1990}
}

@inproceedings{ergo,
 author = {Bobot, Fran\c{c}ois and Conchon, Sylvain and Contejean, Evelyne and Lescuyer, St\'{e}phane},
 title = {{Implementing polymorphism in SMT solvers}},
 booktitle = {SMT '08/BPR '08: Proceedings of the Joint Workshops of the 6th International Workshop on Satisfiability Modulo Theories and 1st International Workshop on Bit-Precise Reasoning},
 year = {2008},
 isbn = {978-1-60558-440-9},
 pages = {1--5},
 location = {Princeton, New Jersey},
 doi = {http://doi.acm.org/10.1145/1512464.1512466},
 publisher = {ACM},
 address = {New York, NY, USA},
 }


@article{vcc,
  title = {VCC: A Practical System for Verifying Concurrent C},
  author = {Ernie Cohen, Markus Dahlweid, Mark Hillebrand, Dirk Leinenbach, Micha? Moskal, Thomas Santen, Wolfram Schulte and Stephan Tobies},
  journal = {Lecture Notes in Computer Science, 5674, Theorem Proving in Higher Order Logics},
  publisher = {Springer Berlin / Heidelberg},
  year = {2009}
}

@article{Hypervisor,
  title = {Verifying the Microsoft Hyper-V Hypervisor with VCC},
  author = {Dirk Leinenbach and Thomas Santen},
  journal = {Lecture Notes in Computer Science, 5850, FM: Formal Methods},
  publisher = {Springer Berlin / Heidelberg},
  year = {2009}
}

@article{z3,
  title = {Z3: An Efficient SMT Solver},
  author = {Leonardo de Moura and Nikolaj Bjorne},
  journal = {Lecture Notes in Computer Science},
  publisher = {Springer Berlin / Heidelberg},
  year = {2008},
  pages = {337-340}
}
 
@inproceedings{bolingbroke10supercompilation,
 author = {Bolingbroke, Maximilian and Peyton Jones, Simon},
 title = {Supercompilation by evaluation},
 booktitle = {Haskell '10: Proceedings of the third ACM Haskell symposium on Haskell},
 year = {2010},
 isbn = {978-1-4503-0252-4},
 pages = {135--146},
 location = {Baltimore, Maryland, USA},
 doi = {http://doi.acm.org/10.1145/1863523.1863540},
 publisher = {ACM},
 address = {New York, NY, USA},
 }

@inproceedings{danaesch,
 author = {Dana Xu and Simon Peyton-Jones and Koen Claesen},
 title = {Static {C}ontract {C}hecking for {H}askell},
 booktitle = {POPL},
 year = {2009}
 }

 @inproceedings{hinze06typedcontracts,
    author = {Ralf Hinze and Johan Jeuring and Andres L\"{o}h},
    title = {Typed contracts for functional programming},
    booktitle = {In FLOPS '06: Functional and Logic Programming: 8th International Symposium},
    year = {2006},
    pages = {208--225},
    publisher = {Springer-Verlag}
}

@inproceedings{agda,
    abstract = {Dependently typed languages have for a long time been used to describe proofs about programs. Traditionally, dependent types are used mostly for stating and proving the properties of the programs and not in defining the programs themselves. An impressive example is the certified compiler by Leroy (2006) implemented and proved correct in Coq (Bertot and Cast\&\#233;ran 2004).},
    address = {New York, NY, USA},
    author = {Norell, Ulf},
    booktitle = {TLDI '09: Proceedings of the 4th international workshop on Types in language design and implementation},
    citeulike-article-id = {4463453},
    citeulike-linkout-0 = {http://portal.acm.org/citation.cfm?id=1481862},
    citeulike-linkout-1 = {http://dx.doi.org/10.1145/1481861.1481862},
    doi = {10.1145/1481861.1481862},
    isbn = {978-1-60558-420-1},
    keywords = {agda, dependent\_types},
    location = {Savannah, GA, USA},
    pages = {1--2},
    posted-at = {2010-08-27 14:10:40},
    priority = {0},
    publisher = {ACM},
    title = {{Dependently typed programming in Agda}},
    doi = {http://dx.doi.org/10.1145/1481861.1481862S},
    year = {2009}
}

 
@book{coq,
    author = {Bertot, Yves and Cast{\'{e}}ran, Pierre},
    citeulike-article-id = {2868779},
    citeulike-linkout-0 = {http://www.labri.fr/perso/casteran/CoqArt/index.html},
    keywords = {coq},
    posted-at = {2008-06-06 09:20:28},
    priority = {0},
    publisher = {Springer-Verlag},
    title = {{Interactive Theorem Proving and Program Development, Coq'Art:the Calculus of Inductive Constructions}},
    year = {2004}
}

@MISC{isacosy,
    author = {Moa Johansson and Lucas Dixon and Alan Bundy},
    title = {{Conjecture Synthesis for Inductive Theories}},
    year = {2010}
}

@inproceedings{smallfoot,
  author    = {Josh Berdine and Cristiano Calcagno and Peter O'Hearn},
  title     = {{Smallfoot: Modular Automatic Assertion Checking with Separation Logic}},
  booktitle = {FMCO},
  year      = {2005}
}

@inproceedings{refinement1,
 author = {Kawaguchi, Ming and Rondon, Patrick and Jhala, Ranjit},
 title = {Type-based data structure verification},
 booktitle = {Proceedings of the 2009 ACM SIGPLAN conference on Programming language design and implementation},
 series = {PLDI '09},
 year = {2009},
 isbn = {978-1-60558-392-1},
 location = {Dublin, Ireland},
 pages = {304--315},
 numpages = {12},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {dependent types, hindley-milner, predicate abstraction, type inference},
} 

@inproceedings{refinement2,
 author = {Freeman, Tim and Pfenning, Frank},
 title = {{Refinement types for ML}},
 booktitle = {Proceedings of the ACM SIGPLAN 1991 conference on Programming language design and implementation},
 series = {PLDI '91},
 year = {1991},
 isbn = {0-89791-428-7},
 location = {Toronto, Ontario, Canada},
 pages = {268--277},
 numpages = {10},
 publisher = {ACM},
 address = {New York, NY, USA},
} 